<html>
<head><meta charset="utf-8"><title>proving things · wg-secure-code · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/index.html">wg-secure-code</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/proving.20things.html">proving things</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="136720077"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/proving%20things/near/136720077" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/proving.20things.html#136720077">(Oct 29 2018 at 17:04)</a>:</h4>
<p>Hey <span class="user-mention" data-user-id="120791">@RalfJ</span> and maybe others:</p>
<p>I have a question. I am working on <a href="https://github.com/salsa-rs/salsa" target="_blank" title="https://github.com/salsa-rs/salsa">salsa</a> some in my spare time, which is a re-implementation of the incremental infrastructure from the compiler. It uses some read-write locks and a bit of error-prone logic that I've already gotten wrong a few times -- basically I have to reason about "all possible interleavings" which is hard to do. After the latest bug, I wanted to try and get more systematic in my approach. I can try to work this out on pen+paper (and probably will), but I was wondering if there is a nice "lightweight" tool that would let me try to encode the states I think and help me to reason about the interleavings. It feels like something that I ought to be able to use... I don't know ... Coq for or something. =)</p>



<a name="136720090"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/proving%20things/near/136720090" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/proving.20things.html#136720090">(Oct 29 2018 at 17:04)</a>:</h4>
<p>I put this in this area because this feels like the sort of thing secure code might also want to do...</p>



<a name="136720101"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/proving%20things/near/136720101" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/proving.20things.html#136720101">(Oct 29 2018 at 17:04)</a>:</h4>
<p>...I know for Rayon I've often wanted to do similar things, though in that case I am reasoning about unsafe code, which makes things all the more fun.</p>



<a name="136720120"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/proving%20things/near/136720120" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/proving.20things.html#136720120">(Oct 29 2018 at 17:05)</a>:</h4>
<p>oh hey I see a similar topic <code>correctness proofs</code>...</p>



<a name="136725916"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/proving%20things/near/136725916" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/proving.20things.html#136725916">(Oct 29 2018 at 18:34)</a>:</h4>
<p>if you ask me I'll tell you you don't want to think about interleavings. instead you want to think about ownership, in the sense of separation logic. :D</p>



<a name="136725992"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/proving%20things/near/136725992" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/proving.20things.html#136725992">(Oct 29 2018 at 18:35)</a>:</h4>
<p>reasoning about concurrent code by looking at interleavings is like reasoning about sequential code by considering assembly-level details like registers. it works, if you are willing to suffer, but you really ought to work with a higher-level abstraction if you can (and most of the time, you can).</p>



<a name="136726109"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/proving%20things/near/136726109" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/proving.20things.html#136726109">(Oct 29 2018 at 18:37)</a>:</h4>
<p>but unfortunately I don't know much about tools for doing this kind of reasoning. If you want to do it in Coq, sure, there are some frameworks you can use (and I am author of one of them), but that's pretty complex stuff and takes a long time to get into</p>



<a name="136726156"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/proving%20things/near/136726156" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/proving.20things.html#136726156">(Oct 29 2018 at 18:38)</a>:</h4>
<p>there are some tools but I am not deeply familiar with any of them</p>



<a name="136726173"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/proving%20things/near/136726173" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/proving.20things.html#136726173">(Oct 29 2018 at 18:38)</a>:</h4>
<p>but what about asking in the wg-verification gitter at <a href="https://gitter.im/rust-lang/wg-verification" target="_blank" title="https://gitter.im/rust-lang/wg-verification">https://gitter.im/rust-lang/wg-verification</a> ? some of these tools' authors are there :P</p>



<a name="136727232"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/proving%20things/near/136727232" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/proving.20things.html#136727232">(Oct 29 2018 at 18:55)</a>:</h4>
<blockquote>
<p>if you ask me I'll tell you you don't want to think about interleavings. instead you want to think about ownership, in the sense of separation logic. :D</p>
</blockquote>
<p>You're not wrong about this, and it is kind of what I've been doing -- I basically want to show that the "ownership model" I have in my head is correctly implemented, I guess.. I have to think about it. To be honest talking about "tools" is the wrong thing, I should start by just writing in English the protocol which I'm sure will help 100x</p>



<a name="136728648"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/proving%20things/near/136728648" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/proving.20things.html#136728648">(Oct 29 2018 at 19:19)</a>:</h4>
<p>bonus points if you use separation logic instead of English :)</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>